$\vdash$  $\forall$$A$, $B$:Type. $A$ $\equiv$ $B$ $\in$ $\mathbb{P}$